#include <iostream>
#include <fstream>
#include <cstdlib>
#include "Minisat.h"
#include "Sat.h"


using namespace std;

Minisat::Minisat(GraphInterface * graph, int coverSize) : g(graph), coverSize(coverSize), sat(g->getSize() * coverSize)
{
}

Minisat::~Minisat() 
{
}

void Minisat::vcProblemToSat() 
{   
  for(int i = 0; i < g->getSize(); ++i)
    for(int j = 1; j <= coverSize - 1; ++j)
      {

	for(int k = j + 1; k <= coverSize; ++k)
	  {
	    vector<int> clause;
	    clause.push_back( -(i * coverSize + j));
	    clause.push_back( -(i * coverSize + k));
	    sat.addClause(clause);
	  }
      }      

  for(int i = 1; i <= coverSize; ++i)
    for(int j = 0; j < g->getSize() - 1; ++j)
      {
	for(int k = j + 1; k < g->getSize(); ++k)
	  {
	    vector<int> clause;
	    clause.push_back( -(j * coverSize + i));
	    clause.push_back( -(k * coverSize + i));
	    sat.addClause(clause);
	  }    
      }
  
  for(int u = 0; u < g->getSize(); ++u)
    {
      vector<int> neighbs = g->neighbours(u);
      for(int j = 0; j < neighbs.size(); ++j)
	{
	  int v = neighbs[j];
	  vector<int> clause;
	  for(int k = 1; k <= coverSize; ++k)
	    {
	      clause.push_back(u * coverSize + k);
	      clause.push_back(v * coverSize + k);
	    }
	
	  sat.addClause(clause);
	} 
    }  
  sat.writeInfile();
  sat.runMinisat();
}

vector<int> Minisat::satProblemToVc()
{
  bool b = sat.readOutfile();
  vector<int> tmp = sat.getCover();
  vector<int> result;
 
  if (!b)
    return result;
  
  for(int i = 0; i < tmp.size(); ++i)
    {
      result.push_back(((tmp[i] - 1) / coverSize) + 1);
    }
  
  return result;
}
